(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun shifted1_value1 () String)
(declare-fun f () String)
(declare-fun g () String)
(assert (not (str.contains f "H")))
(assert (and (not (str.contains (str.substr c 0 (str.len f)) "G")) (not (str.contains (str.substr c 0 (str.len f)) "F"))))
(assert (= d "cachecontrol"))
(assert (and (not (str.contains f "E")) (not (str.contains f "D")) (not (str.contains f "C"))))
(assert (and (not (str.contains (str.substr c 0 (str.len f)) "A")) (not (= (str.at (str.substr c 0 (str.len f)) (- (str.len f) 1)) "\v"))))
(assert (not (= (str.at f (- (str.len f) 1)) "\r")))
(assert (and (not (= (str.at (str.substr c 0 (str.len f)) (- (str.len (str.substr c 0 (str.len f))) 1)) "\n")) (not (= (str.at (str.substr c 0 (str.len f)) (- (str.len f) 1)) "\t")) (not (= (str.at (str.substr c 0 (str.len f)) (- (str.len f) 1)) " "))))
(assert (not (= (str.at f 0) "\f")))
(assert (and (not (= (str.at (str.substr c 0 (str.len f)) 0) "\v")) (not (= (str.at (str.substr c 0 (str.len f)) 0) "\r"))))
(assert (and (not (= (str.at (str.substr c 0 (str.len f)) 0) "\v")) (not (= (str.at (str.substr c 0 (str.len f)) 0) "\r"))))
(assert (and (not (= (str.at f 0) "\n")) (not (= (str.at f 0) "\t")) (= (str.indexof f "=" 0) (- 1)) (not (= (str.len f) 0))))
(assert (and (not (= (str.at (str.substr c 0 (str.len f)) 0) " ")) (= (str.indexof (str.substr c 0 (str.len f)) "=" 0) (- 1))))
(assert (not (str.contains f ",")))
(assert (<= 0 (+ (str.indexof (str.substr shifted1_value1 0 (str.indexof (str.substr b 0 (str.len shifted1_value1)) "=" 0)) "N" 0) 1)))
(assert (<= 0 (- (str.len (str.substr (str.substr b 0 (str.len shifted1_value1)) 0 (- (str.indexof shifted1_value1 "=" 0) 0))) (+ (str.indexof (str.substr (str.substr b 0 (str.len shifted1_value1)) 0 (- (str.indexof shifted1_value1 "=" 0) 0)) "N" 0) 1))))
(assert (<= 0 (- (+ (str.indexof (str.substr (str.substr b 0 (str.len shifted1_value1)) 0 (str.indexof (str.substr b 0 (str.len shifted1_value1)) "=" 0)) "N" 0) 1))))
(assert (<= 0 (+ (str.indexof (str.substr (str.substr b 0 (str.len shifted1_value1)) 0 (- (str.indexof shifted1_value1 "=" 0) 0)) "N" 0) 1)))
(assert (<= 0 (- (str.len (str.substr shifted1_value1 0 (- (str.indexof (str.substr b 0 (str.len shifted1_value1)) "=" 0) 0))) (+ (str.indexof (str.substr shifted1_value1 0 (- (str.indexof (str.substr b 0 (str.len shifted1_value1)) "=" 0) 0)) "N" 0) 1))))
(assert (<= 0 (- (str.len (str.substr shifted1_value1 0 (- (str.indexof (str.substr b 0 (str.len shifted1_value1)) "=" 0) 0))) (+ (str.indexof (str.substr shifted1_value1 0 (- (str.indexof (str.substr b 0 (str.len shifted1_value1)) "=" 0) 0)) "N" 0) 1))))
(assert (<= 0 (- (str.len (str.substr shifted1_value1 0 (- (str.indexof shifted1_value1 "=" 0) 0))) (+ (str.indexof (str.substr shifted1_value1 0 (- (str.indexof shifted1_value1 "=" 0) 0)) "N" 0) 1))))
(assert (<= 0 (str.indexof (str.substr b 0 (str.len shifted1_value1)) "=" 0)))
(assert (<= 0 (- (str.indexof shifted1_value1 "=" 0))))
(assert (<= 0 (+ (str.indexof (str.substr b 0 (str.len shifted1_value1)) "=" 0) 1)))
(assert (<= 0 (- (str.len (str.substr b 0 (str.len shifted1_value1))) (+ (str.indexof shifted1_value1 "=" 0) 1))))
(assert (<= 0 (- (+ (str.indexof (str.substr c 0 (str.len f)) "S" 0) 1))))
(assert (<= 0 (- (str.len f) (+ (str.indexof f "S" 0) 1))))
(assert (<= 0 (- (str.len (str.substr c 0 (str.len f))) (+ (str.indexof (str.substr c 0 (str.len f)) "S" 0) 1))))
(assert (<= 0 (+ (str.indexof f "S" 0) 1)))
(assert (<= 0 (+ (str.indexof (str.substr c 0 (str.len f)) "S" 0) 1)))
(assert (<= 0 (- (str.len (str.substr c 0 (str.len f))) (+ (str.indexof f "S" 0) 1))))
(assert (= (not (= "" g)) true (= (str.replace (str.replace a d "") "Pkgwt" "") "Example:")))
(assert (= a (str.++ (str.++ d "Pkgwt") g)))
(assert (= b (str.++ shifted1_value1 g)))
(assert (= c (str.++ f g)))
(check-sat)
